-- MAIN == 15
DEF MAIN:nat == mul(3,5)
